\section{Background}
In the following we write $P$ for the set of atomic propositions and $\olP := \setx{\olp}{p \in P}$ for the set of negated propositions of $P$. We write $\true$ for \emph{true} and $\false$ for \emph{false}, and $\Sigma$ for the set $2^P$.


% ========== Alternating Automaton
Let $P':= P \cup \olP \cup \set{\true, \false}$. We also fix $\bbD := \set{-1,0,1}$ as the set of directions and $\bbD' := \bbD \cup \set{\opZ}$. A \emph{2-way alternating automaton} $\autA=(Q,\delta,\qI,F)$ over $P$ is a tuple, where $Q$ is a finite set of states, $\delta: Q \to \calB^+(P' \cup (Q \times \bbD'))$ is the transition function, $\qI \in Q$ is the initial state, and $F \subseteq Q$ is the acceptance set. The \emph{size} $|\autA|$ of the automaton $\autA$ is $|Q|$.  


A \emph{run} of $\autA$ on a word $w \in \Sigma^\omega$ is a tree $r:T \to P' \cup (Q \times \bbN)$ such that $r(\epsilon) = (\qI,0)$ and for each node $x \in T$ with $r(x)=(q,h)$, we have
\begin{enumerate}
	\item $\false \notin L$,
	\item $w_h \models 
		(\bigwedge_{p \in L \cap P} p) \land 
		(\bigwedge_{p \in L \cap \olP} \neg p)$,\quad and
	%
	\item $L \cup \Setx{(q', h'-h) \in Q \times \bbZ}{r(y) = (q', h'), \text{ where $y$ is a child of $x$}} \minmodels \delta'(q)$,
\end{enumerate}
where $L := \setx{r(y) \in P}{\text{$y$ is a child of $x$}}$, and $\delta'(q) := \delta(q)[\true / (s,Z)]$ if $h=0$ and $\delta(q)[(s,-1) / (s,Z)]$ if $h \neq 0$. Note that $w_h$ is the $h^{th}$ letter of $w$. A \emph{configuration} of $\autA$ is a pair $(q,h)\in Q\times \bbN$ consisting of the current state and the position of the read-only head in the input word. For a sequence of configurations $v := (q_0,h_0)(q_1,h_1)\dots \in (Q \times \bbN)^\omega$, we define $\inf(v)$ as the set of states that occur infinitely often in $q_0q_1q_2\dots \in Q^\omega$. An infinite path $v$ in $T$ is \emph{accepting} if $r(v_i) \in Q \times \bbN$, for all $i \in \bbN$, and $\inf(v) \cap F \neq \emptyset$. The run $r$ is \emph{accepting} if every infinite path in $r$ is accepting. The \emph{language} of $\autA$ is the set $L(\autA) := \setx{w\in\Sigma^\omega}{\text{there is an accepting run of $\autA$ on $w$}}$.

An ABA is called \emph{locally 1-way} if for every $q \in Q$ there is no minimal model of  $\delta(q)$ that contains $(p, -1)$ and $(s, 1)$, for some $p, s \in Q$.


% ========== Nondeterministic Automaton
We call an ABA \emph{nondeterministic}, NBA for short, if for every state $q\in Q$, each monomial in the DNF of $\delta(q)$ contains at most one tuple in $Q \times \bbD'$. We call an ABA \emph{universal}, UBA for short, if for every state $q\in Q$, each clause in the CNF of $\delta(q)$ contains at most one tuple in $Q \times \bbD'$. For these class of automata, we overload notation and write $\delta:Q \to 2^{\calB^+(P') \times (Q \times \bbD')}$, when the branching type is known.



\ignore{
Let $\bbN := \set{1,\dots}$ and $\bbN_0 := \set{0} \cup \bbN$ be the set of natural numbers.

% ========== Words
Given an alphabet $\Sigma$, $\Sigma^*$ is the set of finite words over
$\Sigma$ and $\Sigma^\omega$ is the set of infinite words over
$\Sigma$.  Let $w$ be a word over $\Sigma$. We denote its length by
$|w|$.  Note that $|w|=\infty$ if $w\in\Sigma^{\omega}$.  For $i<|w|$,
$w_i$ denotes the $i$th letter of $w$, and we write $w^i$ for the word
$w_0w_1\dots w_{i-1}$, where $i\in\bbN_0 \cup\{\infty\}$ with $i\leq
|w|$.  The word $u\in\Sigma^*\cup\Sigma^{\omega}$ is a \emph{prefix}
of $w$ if $w^i=u$, for some $i\in\bbN_0\cup\{\infty\}$ with $i\leq |w|$.

% ========== Trees
A ($\Sigma$-labeled) \emph{tree} is a function $t:T\to\Sigma$, where $T\subseteq\bbN^*$ satisfies the following conditions: 
\begin{inparaenum}[$(i)$]
	\item $T$ is prefix-closed (i.e., if $w\in T$ and $u$ is a prefix of $w$ then $u\in T$) and 
	\item if $xc\in T$ and $c>1$ then $x(c-1)\in T$.
\end{inparaenum}
%%
The elements in $T$ are called the \emph{nodes} of $t$ and the empty word $\epsilon$ is called the \emph{root} of $t$.  A node $xc\in T$ with $c\in\bbN$ is called a \emph{child} of the node $x\in T$. We call $t$ \emph{$k$-ary} if every node in $t$ has $k$ children.
%%
%With $t_{\upharpoonright U}$ we denote the restriction of $r$ to the
%domain $U\subseteq T$, i.e., $t_{\upharpoonright U}$ is the function
%$t_{\upharpoonright U}:U\rightarrow \Sigma$ with $t_{\upharpoonright
%  U}(x)=t(x)$, for all $x\in U$.
%%
An (infinite) \emph{path} in $t$ is a word $\pi\in\bbN^{\omega}$ such
that $u\in T$, for every prefix $u$ of $\pi$. We write $t(\pi)$ for
the word $t(\pi^0) t(\pi^1)\dots\in\Sigma^{\omega}$.


% ========== Propositional logic	
For a set $P$ of propositions, $\calB^+(P)$ is the set of \emph{positive Boolean formulas} over $P$, i.e., the formulas built from the propositions in $P$, and the connectives $\land$ and $\lor$. Given $M\subseteq P$ and $\beta \in \calB^+(P)$, we write $M\models\beta$ if the $\beta$ evaluates to true when assigning true to the propositions in $M$ and false to propositions in $P \setminus M$. Moreover, we write $M\minmodels\beta$ if $M$ is a \emph{minimal model} of $\beta$, i.e., $M\models\beta$ and there is no $p\in M$ such that $M\setminus\{p\}\models\beta$. 




% ========== acceptance conditions
Note that we do not have any restriction on the acceptance condition
$\calF$; it can be any subset of $Q^{\omega}$.  However, since this is
often too general, one usually considers automata where the acceptance
conditions are specified in a certain finite way---the \emph{type} of
an acceptance condition. Commonly used types of acceptance conditions
are listed in Table~\ref{tab:acctypes}. Here, $\inf(\pi)$ is the set
of states that occur infinitely often in $\pi\in Q^\omega$ and the
integer $k$ is called the \emph{index} of the automaton.  If $\calF$
is specified by the type $\tau$, we say that $\autA$ is a $\tau$
automaton.  Moreover, if the type of the acceptance condition is clear
from the context, we just give the finite description $\alpha$ instead
of $\calF$. For instance, a B\"uchi automaton is given as a tuple
$(S,\Gamma,\eta,s_{\rmI},\alpha)$ with $\alpha\subseteq S$.
\begin{table}[t]
  \footnotesize
  \begin{tabularx}{\linewidth}{p{3.5cm}X}
    \truerule
    type: $\tau$ & 
    finite description, acceptance condition: $\alpha$, $\calF$ 
    \\
    % \cmidrule(r){1-1}\cmidrule(r){2-2}
    % & $\alpha = F \subseteq Q$  \\
    % finite	& $\calF := \{q_0 q_1 \dots q_n \in Q^* ~|~ q_n \in F \}$  \\
    % co-finite	& $\calF := \{q_0 q_1 \dots q_n \in Q^* ~|~ q_n \notin F \}$  \\
    % 
    \cmidrule(r){1-1}\cmidrule(r){2-2}
    & $\alpha = F \subseteq Q$  
    \\
    B\"uchi	& 
    $\calF := \setx{\pi \in Q^\omega}{\inf(\pi) \cap F \neq \emptyset}$  
    \\
    co-B\"uchi  &  
    $\calF := \setx{\pi \in Q^\omega}{\inf(\pi) \cap F = \emptyset}$  
    \\
    \cmidrule(r){1-1}\cmidrule(r){2-2}
    & $\alpha = \{F_1,\dots,F_{2k}\} \subseteq 2^Q$, where 
    $F_1 \subseteq F_2 \subseteq \dots \subseteq F_{2k}$  
    \\
    parity	& 
    $\calF := \setx{\pi \in Q^\omega}
    {\min\set{i}{F_i\cap\inf(\pi)\ne\emptyset}\text{ is even}}$ 
    \\
    co-parity & 
    $\calF := \setx{\pi \in Q^\omega}
    {\min\set{i}{F_i \cap \inf(\pi)\ne\emptyset}\text{ is odd}}$ 
    \\
    \cmidrule(r){1-1}\cmidrule(r){2-2}
    & $\alpha = \{(B_1,C_1),\dots,(B_k,C_k)\} \subseteq 2^Q\times 2^Q$  
    \\
    Rabin	& 
    $\calF := \bigcup_i \setx{\pi \in Q^\omega}{\inf(\pi) \cap B_i \neq
      \emptyset \text{ and } \inf(\pi) \cap C_i = \emptyset}$
    \\
    Streett & 
    $\calF := \bigcap_i \setx{\pi \in Q^\omega}
    {\inf(\pi) \cap B_i = \emptyset \text{ or } 
      \inf(\pi) \cap C_i \neq \emptyset}$  
    \\
    \cmidrule(r){1-1}\cmidrule(r){2-2}
    & $\alpha = \{M_1,\dots,M_k\} \subseteq 2^Q$  
    \\
    Muller & 
    $\calF := \bigcup_i \setx{\pi \in Q^\omega}{\inf(\pi) = M_i}$  
    \\
%    co-Muller & 
%    $\calF := \bigcap_i \set{\pi \in Q^\omega}{\inf(\pi) \neq M_i}$  
%    \\
    % Generalized B\"uchi	& 
    % $\calF := \bigcap_i \set{\pi \in Q^\omega}
    % {\inf(\pi) \cap M_i \neq \emptyset}$
    % \\
    \bottomrule
  \end{tabularx}
  \caption{Types of acceptance conditions.}
  \label{tab:acctypes}
\end{table}

% ========== 1-way
The automaton $\autA$ is \emph{1-way} if $-1 \notin \bbD$. That means, $\autA$ cannot move the read-only head back towards the root.
% ========== Branching modes
The automaton $\autA$ is \emph{nondeterministic} if $\delta$ returns a disjunction for all inputs; $\autA$ is \emph{universal} if $\delta$ returns a conjunction for all inputs; $\autA$ is \emph{deterministic} if it is nondeterministic and universal.
%%%
%For nondeterministic and deterministic automata, we use standard
%notation. For instance, if $\autA$ is nondeterministic, we view
%$\delta$ as a function of the form $\delta:
%Q\rightarrow2^{Q\times\bbD}$. That means, a clause is written as a
%set.  Note that a run $r:T\to Q\times \bbN$ of a nondeterministic
%automaton $\autA$ on $w\in\Sigma^{\omega}$ consists of the single path
%$\pi = 0^\omega$. To increase readability, we call $r(\pi) \in
%(Q\times \bbN)^\omega$ also a run of $\autA$ on $w$.
%%%
%Moreover, for $R\subseteq Q$ and $a\in \Sigma$, we abbreviate
%$\bigcup_{q\in R} \delta(q,a)$ by $\delta(R,a)$.
}